C:(IdType), A, B:Type, L2:((tg:Id  (AB(C(tg) List))) List),
L:((l:IdLnk  (t:Id  C(t))) List), tg:Id, a:A, b:B.
{(map(x.x.2;L) = concat(map(tgf.map(x.<tgf.1, x>;(tgf.2)(a,b));L2))  ((tg:Id  C(tg)) List))
 ((tg  map(p.p.1;L2)))
 (||filter(ms.(ms.2).1 = tg;L)|| = 0)} 

latex

Definitions	P  Q, P & Q, P  Q, (x  l), , concat(ll), map(f;as), t.1, t.2, x. t(x), A, False, P  Q, suptype(S; T), Id, x(s), IdLnk, S  T, x:A. B(x), Top, t  T, {T}
Lemmas	top wf, map-concat-filter-lemma1, Id wf, IdLnk wf, pi2 wf, pi1 wf, map wf, concat wf, l member wf, not wf, length zero